Nuprl Lemma : mul_functionality_wrt_eq
13,42
postcript
pdf
i1
,
i2
,
j1
,
j2
:
. (
i1
=
j1
)
(
i2
=
j2
)
((
i1
*
i2
) = (
j1
*
j2
))
latex
Up
int
2
,
int
2
Definitions
,
t
T
,
P
Q
,
x
:
A
.
B
(
x
)
origin
i1, i2, j1, j2:
. (i1 = j1) 
(i2 = j2) ((i1 * i2) = (j1 * j2)) i1, i2, j1, j2:. (i1 = j1) (i2 = j2) ((i1 * i2) = (j1 * j2)) 
T Qx:A. B(x)